T:Type, L:T List, P:(TProp).
(x:||L||. Dec(P(L[x])))
 (i, j:||L||. P(L[i])  i<j  P(L[j]))
 (L1, L2:T List.
 (L = (L1 @ L2) & (i:||L1||. P(L1[i])) & (i:||L2||. P(L2[i]))
 (& (xL. P(x)  (x  L2))) 

latex

Definitions	t  T, x:A. B(x), ||as||, P  Q, False, A, P & Q, AB, i  j < k, {i..j}, (x  l), Prop, x. t(x), xL. P(x), l[i], as @ bs, x:A. B(x), Dec(P), P  Q, hd(l), i<j, ij, ij, P  Q, P  Q, {T}, SQType(T), , A & B, True, T
Lemmas	squash wf, true wf, cons member, length cons, l all cons, select cons tl, decidable int equal, length zero, select append front, length append, decidable lt, non neg length, select cons tl sq, le wf, l all nil, decidable wf, length wf2, append wf, not wf, int seg wf, length wf1, select wf, l all wf, l member wf